Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

nats_active -> add_active1(zeros_active)
hd_active1(x) -> hd1(x)
zeros_active -> cons2(0, zeros)
tl_active1(x) -> tl1(x)
incr_active1(cons2(x, y)) -> cons2(s1(x), incr1(y))
mark1(nats) -> nats_active
add_active1(cons2(x, y)) -> incr_active1(cons2(x, add1(y)))
mark1(zeros) -> zeros_active
hd_active1(cons2(x, y)) -> mark1(x)
mark1(incr1(x)) -> incr_active1(mark1(x))
tl_active1(cons2(x, y)) -> mark1(y)
mark1(add1(x)) -> add_active1(mark1(x))
nats_active -> nats
mark1(hd1(x)) -> hd_active1(mark1(x))
zeros_active -> zeros
mark1(tl1(x)) -> tl_active1(mark1(x))
incr_active1(x) -> incr1(x)
mark1(0) -> 0
add_active1(x) -> add1(x)
mark1(s1(x)) -> s1(x)
mark1(cons2(x, y)) -> cons2(x, y)

Q is empty.


QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

nats_active -> add_active1(zeros_active)
hd_active1(x) -> hd1(x)
zeros_active -> cons2(0, zeros)
tl_active1(x) -> tl1(x)
incr_active1(cons2(x, y)) -> cons2(s1(x), incr1(y))
mark1(nats) -> nats_active
add_active1(cons2(x, y)) -> incr_active1(cons2(x, add1(y)))
mark1(zeros) -> zeros_active
hd_active1(cons2(x, y)) -> mark1(x)
mark1(incr1(x)) -> incr_active1(mark1(x))
tl_active1(cons2(x, y)) -> mark1(y)
mark1(add1(x)) -> add_active1(mark1(x))
nats_active -> nats
mark1(hd1(x)) -> hd_active1(mark1(x))
zeros_active -> zeros
mark1(tl1(x)) -> tl_active1(mark1(x))
incr_active1(x) -> incr1(x)
mark1(0) -> 0
add_active1(x) -> add1(x)
mark1(s1(x)) -> s1(x)
mark1(cons2(x, y)) -> cons2(x, y)

Q is empty.

Q DP problem:
The TRS P consists of the following rules:

MARK1(nats) -> NATS_ACTIVE
MARK1(tl1(x)) -> MARK1(x)
ADD_ACTIVE1(cons2(x, y)) -> INCR_ACTIVE1(cons2(x, add1(y)))
MARK1(tl1(x)) -> TL_ACTIVE1(mark1(x))
MARK1(add1(x)) -> MARK1(x)
HD_ACTIVE1(cons2(x, y)) -> MARK1(x)
MARK1(zeros) -> ZEROS_ACTIVE
MARK1(incr1(x)) -> INCR_ACTIVE1(mark1(x))
MARK1(add1(x)) -> ADD_ACTIVE1(mark1(x))
MARK1(hd1(x)) -> HD_ACTIVE1(mark1(x))
NATS_ACTIVE -> ZEROS_ACTIVE
MARK1(hd1(x)) -> MARK1(x)
NATS_ACTIVE -> ADD_ACTIVE1(zeros_active)
TL_ACTIVE1(cons2(x, y)) -> MARK1(y)
MARK1(incr1(x)) -> MARK1(x)

The TRS R consists of the following rules:

nats_active -> add_active1(zeros_active)
hd_active1(x) -> hd1(x)
zeros_active -> cons2(0, zeros)
tl_active1(x) -> tl1(x)
incr_active1(cons2(x, y)) -> cons2(s1(x), incr1(y))
mark1(nats) -> nats_active
add_active1(cons2(x, y)) -> incr_active1(cons2(x, add1(y)))
mark1(zeros) -> zeros_active
hd_active1(cons2(x, y)) -> mark1(x)
mark1(incr1(x)) -> incr_active1(mark1(x))
tl_active1(cons2(x, y)) -> mark1(y)
mark1(add1(x)) -> add_active1(mark1(x))
nats_active -> nats
mark1(hd1(x)) -> hd_active1(mark1(x))
zeros_active -> zeros
mark1(tl1(x)) -> tl_active1(mark1(x))
incr_active1(x) -> incr1(x)
mark1(0) -> 0
add_active1(x) -> add1(x)
mark1(s1(x)) -> s1(x)
mark1(cons2(x, y)) -> cons2(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MARK1(nats) -> NATS_ACTIVE
MARK1(tl1(x)) -> MARK1(x)
ADD_ACTIVE1(cons2(x, y)) -> INCR_ACTIVE1(cons2(x, add1(y)))
MARK1(tl1(x)) -> TL_ACTIVE1(mark1(x))
MARK1(add1(x)) -> MARK1(x)
HD_ACTIVE1(cons2(x, y)) -> MARK1(x)
MARK1(zeros) -> ZEROS_ACTIVE
MARK1(incr1(x)) -> INCR_ACTIVE1(mark1(x))
MARK1(add1(x)) -> ADD_ACTIVE1(mark1(x))
MARK1(hd1(x)) -> HD_ACTIVE1(mark1(x))
NATS_ACTIVE -> ZEROS_ACTIVE
MARK1(hd1(x)) -> MARK1(x)
NATS_ACTIVE -> ADD_ACTIVE1(zeros_active)
TL_ACTIVE1(cons2(x, y)) -> MARK1(y)
MARK1(incr1(x)) -> MARK1(x)

The TRS R consists of the following rules:

nats_active -> add_active1(zeros_active)
hd_active1(x) -> hd1(x)
zeros_active -> cons2(0, zeros)
tl_active1(x) -> tl1(x)
incr_active1(cons2(x, y)) -> cons2(s1(x), incr1(y))
mark1(nats) -> nats_active
add_active1(cons2(x, y)) -> incr_active1(cons2(x, add1(y)))
mark1(zeros) -> zeros_active
hd_active1(cons2(x, y)) -> mark1(x)
mark1(incr1(x)) -> incr_active1(mark1(x))
tl_active1(cons2(x, y)) -> mark1(y)
mark1(add1(x)) -> add_active1(mark1(x))
nats_active -> nats
mark1(hd1(x)) -> hd_active1(mark1(x))
zeros_active -> zeros
mark1(tl1(x)) -> tl_active1(mark1(x))
incr_active1(x) -> incr1(x)
mark1(0) -> 0
add_active1(x) -> add1(x)
mark1(s1(x)) -> s1(x)
mark1(cons2(x, y)) -> cons2(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 1 SCC with 7 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
QDP

Q DP problem:
The TRS P consists of the following rules:

MARK1(tl1(x)) -> MARK1(x)
MARK1(tl1(x)) -> TL_ACTIVE1(mark1(x))
MARK1(add1(x)) -> MARK1(x)
HD_ACTIVE1(cons2(x, y)) -> MARK1(x)
TL_ACTIVE1(cons2(x, y)) -> MARK1(y)
MARK1(hd1(x)) -> HD_ACTIVE1(mark1(x))
MARK1(incr1(x)) -> MARK1(x)
MARK1(hd1(x)) -> MARK1(x)

The TRS R consists of the following rules:

nats_active -> add_active1(zeros_active)
hd_active1(x) -> hd1(x)
zeros_active -> cons2(0, zeros)
tl_active1(x) -> tl1(x)
incr_active1(cons2(x, y)) -> cons2(s1(x), incr1(y))
mark1(nats) -> nats_active
add_active1(cons2(x, y)) -> incr_active1(cons2(x, add1(y)))
mark1(zeros) -> zeros_active
hd_active1(cons2(x, y)) -> mark1(x)
mark1(incr1(x)) -> incr_active1(mark1(x))
tl_active1(cons2(x, y)) -> mark1(y)
mark1(add1(x)) -> add_active1(mark1(x))
nats_active -> nats
mark1(hd1(x)) -> hd_active1(mark1(x))
zeros_active -> zeros
mark1(tl1(x)) -> tl_active1(mark1(x))
incr_active1(x) -> incr1(x)
mark1(0) -> 0
add_active1(x) -> add1(x)
mark1(s1(x)) -> s1(x)
mark1(cons2(x, y)) -> cons2(x, y)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.